#!/usr/bin/env bash
#
# Author: Makarius
#
# build-jars - build Isabelle/Scala
#
# Requires proper Isabelle settings environment.

## sources

declare -a SOURCES=(
  src/HOL/SPARK/Tools/spark.scala
  src/HOL/Tools/Nitpick/kodkod.scala
  src/Pure/Admin/afp.scala
  src/Pure/Admin/build_csdp.scala
  src/Pure/Admin/build_cygwin.scala
  src/Pure/Admin/build_doc.scala
  src/Pure/Admin/build_e.scala
  src/Pure/Admin/build_fonts.scala
  src/Pure/Admin/build_history.scala
  src/Pure/Admin/build_jdk.scala
  src/Pure/Admin/build_log.scala
  src/Pure/Admin/build_polyml.scala
  src/Pure/Admin/build_release.scala
  src/Pure/Admin/build_spass.scala
  src/Pure/Admin/build_sqlite.scala
  src/Pure/Admin/build_status.scala
  src/Pure/Admin/build_vampire.scala
  src/Pure/Admin/build_verit.scala
  src/Pure/Admin/build_zipperposition.scala
  src/Pure/Admin/check_sources.scala
  src/Pure/Admin/ci_profile.scala
  src/Pure/Admin/components.scala
  src/Pure/Admin/isabelle_cronjob.scala
  src/Pure/Admin/isabelle_devel.scala
  src/Pure/Admin/jenkins.scala
  src/Pure/Admin/other_isabelle.scala
  src/Pure/Concurrent/consumer_thread.scala
  src/Pure/Concurrent/counter.scala
  src/Pure/Concurrent/delay.scala
  src/Pure/Concurrent/event_timer.scala
  src/Pure/Concurrent/future.scala
  src/Pure/Concurrent/isabelle_thread.scala
  src/Pure/Concurrent/mailbox.scala
  src/Pure/Concurrent/par_list.scala
  src/Pure/Concurrent/synchronized.scala
  src/Pure/GUI/color_value.scala
  src/Pure/GUI/desktop_app.scala
  src/Pure/GUI/gui.scala
  src/Pure/GUI/gui_thread.scala
  src/Pure/GUI/popup.scala
  src/Pure/GUI/wrap_panel.scala
  src/Pure/General/antiquote.scala
  src/Pure/General/bytes.scala
  src/Pure/General/cache.scala
  src/Pure/General/codepoint.scala
  src/Pure/General/comment.scala
  src/Pure/General/completion.scala
  src/Pure/General/csv.scala
  src/Pure/General/date.scala
  src/Pure/General/exn.scala
  src/Pure/General/file.scala
  src/Pure/General/file_watcher.scala
  src/Pure/General/graph.scala
  src/Pure/General/graph_display.scala
  src/Pure/General/graphics_file.scala
  src/Pure/General/http.scala
  src/Pure/General/json.scala
  src/Pure/General/linear_set.scala
  src/Pure/General/logger.scala
  src/Pure/General/long_name.scala
  src/Pure/General/mailman.scala
  src/Pure/General/mercurial.scala
  src/Pure/General/multi_map.scala
  src/Pure/General/output.scala
  src/Pure/General/path.scala
  src/Pure/General/position.scala
  src/Pure/General/pretty.scala
  src/Pure/General/properties.scala
  src/Pure/General/rdf.scala
  src/Pure/General/scan.scala
  src/Pure/General/sha1.scala
  src/Pure/General/sql.scala
  src/Pure/General/ssh.scala
  src/Pure/General/symbol.scala
  src/Pure/General/time.scala
  src/Pure/General/timing.scala
  src/Pure/General/untyped.scala
  src/Pure/General/url.scala
  src/Pure/General/utf8.scala
  src/Pure/General/uuid.scala
  src/Pure/General/value.scala
  src/Pure/General/word.scala
  src/Pure/General/xz.scala
  src/Pure/Isar/document_structure.scala
  src/Pure/Isar/keyword.scala
  src/Pure/Isar/line_structure.scala
  src/Pure/Isar/outer_syntax.scala
  src/Pure/Isar/parse.scala
  src/Pure/Isar/token.scala
  src/Pure/ML/ml_console.scala
  src/Pure/ML/ml_lex.scala
  src/Pure/ML/ml_process.scala
  src/Pure/ML/ml_statistics.scala
  src/Pure/ML/ml_syntax.scala
  src/Pure/PIDE/byte_message.scala
  src/Pure/PIDE/command.scala
  src/Pure/PIDE/command_span.scala
  src/Pure/PIDE/document.scala
  src/Pure/PIDE/document_id.scala
  src/Pure/PIDE/document_status.scala
  src/Pure/PIDE/editor.scala
  src/Pure/PIDE/headless.scala
  src/Pure/PIDE/line.scala
  src/Pure/PIDE/markup.scala
  src/Pure/PIDE/markup_tree.scala
  src/Pure/PIDE/protocol.scala
  src/Pure/PIDE/protocol_handlers.scala
  src/Pure/PIDE/protocol_message.scala
  src/Pure/PIDE/prover.scala
  src/Pure/PIDE/query_operation.scala
  src/Pure/PIDE/rendering.scala
  src/Pure/PIDE/resources.scala
  src/Pure/PIDE/session.scala
  src/Pure/PIDE/text.scala
  src/Pure/PIDE/xml.scala
  src/Pure/PIDE/yxml.scala
  src/Pure/ROOT.scala
  src/Pure/System/bash.scala
  src/Pure/System/command_line.scala
  src/Pure/System/cygwin.scala
  src/Pure/System/distribution.scala
  src/Pure/System/executable.scala
  src/Pure/System/getopts.scala
  src/Pure/System/isabelle_charset.scala
  src/Pure/System/isabelle_fonts.scala
  src/Pure/System/isabelle_platform.scala
  src/Pure/System/isabelle_process.scala
  src/Pure/System/isabelle_system.scala
  src/Pure/System/isabelle_tool.scala
  src/Pure/System/java_statistics.scala
  src/Pure/System/linux.scala
  src/Pure/System/mingw.scala
  src/Pure/System/numa.scala
  src/Pure/System/options.scala
  src/Pure/System/platform.scala
  src/Pure/System/posix_interrupt.scala
  src/Pure/System/process_result.scala
  src/Pure/System/progress.scala
  src/Pure/System/scala.scala
  src/Pure/System/system_channel.scala
  src/Pure/System/tty_loop.scala
  src/Pure/Thy/bibtex.scala
  src/Pure/Thy/export.scala
  src/Pure/Thy/export_theory.scala
  src/Pure/Thy/file_format.scala
  src/Pure/Thy/html.scala
  src/Pure/Thy/latex.scala
  src/Pure/Thy/presentation.scala
  src/Pure/Thy/sessions.scala
  src/Pure/Thy/thy_element.scala
  src/Pure/Thy/thy_header.scala
  src/Pure/Thy/thy_syntax.scala
  src/Pure/Tools/build.scala
  src/Pure/Tools/build_docker.scala
  src/Pure/Tools/build_job.scala
  src/Pure/Tools/check_keywords.scala
  src/Pure/Tools/debugger.scala
  src/Pure/Tools/doc.scala
  src/Pure/Tools/dump.scala
  src/Pure/Tools/fontforge.scala
  src/Pure/Tools/java_monitor.scala
  src/Pure/Tools/main.scala
  src/Pure/Tools/mkroot.scala
  src/Pure/Tools/phabricator.scala
  src/Pure/Tools/print_operation.scala
  src/Pure/Tools/profiling_report.scala
  src/Pure/Tools/scala_project.scala
  src/Pure/Tools/server.scala
  src/Pure/Tools/server_commands.scala
  src/Pure/Tools/simplifier_trace.scala
  src/Pure/Tools/spell_checker.scala
  src/Pure/Tools/task_statistics.scala
  src/Pure/Tools/update.scala
  src/Pure/Tools/update_cartouches.scala
  src/Pure/Tools/update_comments.scala
  src/Pure/Tools/update_header.scala
  src/Pure/Tools/update_then.scala
  src/Pure/Tools/update_theorems.scala
  src/Pure/library.scala
  src/Pure/pure_thy.scala
  src/Pure/term.scala
  src/Pure/term_xml.scala
  src/Pure/thm_name.scala
  src/Tools/Graphview/graph_file.scala
  src/Tools/Graphview/graph_panel.scala
  src/Tools/Graphview/graphview.scala
  src/Tools/Graphview/layout.scala
  src/Tools/Graphview/main_panel.scala
  src/Tools/Graphview/metrics.scala
  src/Tools/Graphview/model.scala
  src/Tools/Graphview/mutator.scala
  src/Tools/Graphview/mutator_dialog.scala
  src/Tools/Graphview/mutator_event.scala
  src/Tools/Graphview/popups.scala
  src/Tools/Graphview/shapes.scala
  src/Tools/Graphview/tree_panel.scala
  src/Tools/VSCode/src/build_vscode.scala
  src/Tools/VSCode/src/channel.scala
  src/Tools/VSCode/src/dynamic_output.scala
  src/Tools/VSCode/src/language_server.scala
  src/Tools/VSCode/src/lsp.scala
  src/Tools/VSCode/src/preview_panel.scala
  src/Tools/VSCode/src/state_panel.scala
  src/Tools/VSCode/src/textmate_grammar.scala
  src/Tools/VSCode/src/vscode_model.scala
  src/Tools/VSCode/src/vscode_rendering.scala
  src/Tools/VSCode/src/vscode_resources.scala
  src/Tools/VSCode/src/vscode_spell_checker.scala
)


## diagnostics

PRG="$(basename "$0")"

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS]"
  echo
  echo "  Options are:"
  echo "    -f           fresh build"
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}

[ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment"


## process command line

# options

FRESH=""

while getopts "f" OPT
do
  case "$OPT" in
    f)
      FRESH=true
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

[ "$#" -ne 0 ] && usage


## target

TARGET_DIR="lib/classes"
TARGET_JAR="$TARGET_DIR/Pure.jar"
TARGET_SHASUM="$TARGET_DIR/Pure.shasum"

function target_shasum()
{
  shasum -a1 -b "$TARGET_JAR" "${SOURCES[@]}" 2>/dev/null
}

function target_clean()
{
  rm -rf "$TARGET_DIR"
}

[ -n "$FRESH" ] && target_clean


## build

target_shasum | cmp "$TARGET_SHASUM" >/dev/null 2>/dev/null
if [ "$?" -ne 0 ]; then
  echo "### Building Isabelle/Scala ..."

  target_clean

  BUILD_DIR="$TARGET_DIR/build"
  mkdir -p "$BUILD_DIR"

  (
    export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"
    isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS \
      -d "$BUILD_DIR" "${SOURCES[@]}"
  ) || fail "Failed to compile sources"

  CHARSET_SERVICE="META-INF/services/java.nio.charset.spi.CharsetProvider"
  mkdir -p "$BUILD_DIR/$(dirname "$CHARSET_SERVICE")"
  echo isabelle.Isabelle_Charset_Provider > "$BUILD_DIR/$CHARSET_SERVICE"

  cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" "$BUILD_DIR/isabelle/."
  cp "$ISABELLE_HOME/lib/logo/isabelle_transparent.gif" "$BUILD_DIR/isabelle/."

  isabelle_jdk jar -c -f "$(platform_path "$TARGET_JAR")" -e isabelle.Main \
    -C "$BUILD_DIR" META-INF \
    -C "$BUILD_DIR" isabelle || fail "Failed to produce $TARGET_JAR"

  rm -rf "$BUILD_DIR"

  target_shasum > "$TARGET_SHASUM"
fi
